/*
 * $Id: ProtocolUsageMonitor.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.checker.utils;

import java.io.IOException;
import java.io.OutputStream;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedList;

import org.objectweb.fractal.bpc.checker.node.*;

/**
 * This class accepts notificationm about event usage while traversing the state space
 * and is able to print out the coloured protocol usage with emphasizing events not used
 * during the traversal.
 */
public class ProtocolUsageMonitor {

    /**
     * Notifies the class about event being generated be the parse tree
     * @param eventidx Event index.
     * @param node Corresponding parse tree leaf.
     */
    public static void eventGenerated(int eventidx, EventNode node) {

        Integer key = new Integer(eventidx);
        if (table.containsKey(key)) {
            ((LinkedList)table.get(key)).add(node);
        }
        else {
            LinkedList list = new LinkedList();
            list.add(node);
            table.put(key,list);
        }
    }
    
    
    /**
     * Notifies the class about event being really executed.
     * @param eventidx Event index of the event being executed.
     */
    public static void eventExecuted(int eventidx) {
    
		//if (lock)
		//	System.out.println(":::Multiple access to monitor!!!");
			
		//lock = true;
        LinkedList list = (LinkedList)table.get(new Integer(eventidx));
        
        //if (list == null) {
				//	System.out.println("::List null: " + eventidx);
			//		System.out.println("::List size: " + table.size());
			//	}
			
        //if (list != null)
        	for (Iterator it = list.iterator(); it.hasNext(); ) {
          	  ((EventNode)it.next()).setExecuted();
        	}
        
        table.clear();
    }

    /**
     * Notifies the class of execution of an accept event and an emit event, which together form one tau event.
     * @param acceptEventIdx Event index of the accept event being executed.
     * @param emitEventIdx Event index of the emit event being executed.
     */
    public static void eventsExecuted(int acceptEventIdx, int emitEventIdx) {
    
        LinkedList list1 = (LinkedList)table.get(new Integer(acceptEventIdx));
        for (Iterator it1 = list1.iterator(); it1.hasNext(); ) {
            ((EventNode)it1.next()).setExecuted();
        }

        LinkedList list2 = (LinkedList)table.get(new Integer(emitEventIdx));
        for (Iterator it2 = list2.iterator(); it2.hasNext(); ) {
            ((EventNode)it2.next()).setExecuted();
	    }
         
        table.clear();
        //lock = false;
    }

    
    
    /**
     * Public boxing method for printing out the protocol usage as an html output.
     * @param out The stream to write the result to.
     * @param root The top of the parse tree.
     * @throws IOException In the case of an error with writing occurs. 
     */
    public static void printUsage(OutputStream out, TreeNode root) throws IOException {
        out.write(new String("<html><head /><body><pre>\n").getBytes());
        out.write(' ');
        doPrint(out, root, " ");
        out.write(new String("</pre></body></html>\n").getBytes());
    }
    
    /**
     * Printing of the protocol usage as an html stream.
     * @param out The stream to write the result to.
     * @param root The top of the parse tree being written. 
     * @param prefix Formating prefix of spaces.
     * @throws IOException In the case of an exception while writing to the stream.
     */
    private static void doPrint(OutputStream out, TreeNode root, String prefix) throws IOException {
        TreeNode[] children = root.getChildren();
        
        if (root instanceof EventNode) {
            if (!((EventNode)root).getExecuted()) {
                out.write(new String("<strong><font color=\"#FF0000\">").getBytes());
                out.write(root.protocol.getBytes());
                out.write(new String("</font></strong>").getBytes());
            }
            else {
                out.write(root.protocol.getBytes());
                //out.write('\n');
                
            }
        }
        
        // shouldn't happen, but - who cares..
        else if (root instanceof AtomicNode) {
            out.write(root.protocol.getBytes());
            //out.write('\n');
        }
        
        //composite node
        
        else if (root instanceof RepetitionNode) {
            //out.write(prefix.getBytes());
            doPrint(out, children[0], prefix);
            out.write('*');
        }

        else if (root instanceof DeterministicNode) {
            //out.write((prefix + "Det").getBytes());
            doPrint(out, children[0], prefix);
            //out.write((prefix).getBytes());
        }

        else if (root instanceof NullNode) {
            out.write(("NULL").getBytes());
        }

        else {
            //prefix += "   ";
            out.write(new String("(\n" + prefix + "   ").getBytes());
            doPrint(out, children[0], prefix + "   ");
            
            for (int i = 1; i < children.length; ++i) {
             
                if (root instanceof AlternativeNode) {
                    out.write(("\n" + prefix + "+" + "\n" + prefix + "   ").getBytes());
                    doPrint(out, children[i], prefix + "   ");
                }
                
                else if (root instanceof AndParallelNode) {
                    out.write(("\n" + prefix + "|" + "\n" + prefix + "   ").getBytes());
                    doPrint(out, children[i], prefix + "   ");
                }

                else if (root instanceof ConsentNode) {
                    out.write(("\n\n\n" + prefix + "<consent>" + "\n\n\n" + prefix + "   ").getBytes());
                    doPrint(out, children[i], prefix + "   ");
                }
                
                else if (root instanceof SequenceNode) {
                    out.write((" ; ").getBytes());
                    doPrint(out, children[i], prefix + "   ");
                    
                }
            }
            out.write(("\n" + prefix + ")").getBytes());
        }
    }
    
    /**
     * The event usage data.
     * The data are generated and erased each time a transition is really performed.
     */
    private static HashMap table = new HashMap();
    
	//private static boolean lock = false;

}
